preinit1R{$x:ut2, $a:ut2}
preinit1R(i; X; T; x0; P)
== ([@i precondition for "$a"(v:T):
== ([@i s,v. P(s."$x",v) State("$x" : X) v
== (; @i "$x" initially x0:X]) 

latex

---

clarification:

preinit1R{$x:ut2, $a:ut2}
preinit1R(i; X; T; x0; P)
== (@i precondition for "$a"(v:T):
== (@i s,v. P(s."$x",v) State("$x" : X) v
== (.@i "$x" initially x0:X.nil) 

latex

Definitions

(L), @loc precondition for a(v:T):P State(ds) v, x : v, x.A(x), f(a), s.x, car.cdr, @loc x initially v:T, "$x", nil